#!/usr/bin/python
# -*- coding: utf8 -*-

from pyparsing import Literal, White, Regex

from expresion import Expresion, TypeException, Tipo, Exp, TipoExp, makeSintaxis, Id
from lenguaje import Extension

class Func(Tipo):
    
    def __init__(self,tok):
        """
        Define para el tipo funcion el dominio y la imagen.
        """
        dom, img = tok
        self.dominio = dom
        self.imagen = img
    
    def __eq__(self, other):
        """
        Un tipo es igual a un tipo funcion, si es de tipo funcion
        y sus dominios e imagenes son iguales.
        """
        return self.__class__ == other.__class__ and \
                    self.dominio == other.dominio and \
                    self.imagen == other.imagen
    @classmethod
    def sintaxis(cls):
        Abs = makeSintaxis('(', TipoExp, '->' , TipoExp, ')' )
        return Abs
    
    def __str__(self):
        s1 = str(self.dominio)
        s2 = str(self.imagen)
        if self.dominio.__class__ == self.__class__:
            return "(%s) -> %s" % (s1, s2)
        else:
            return "%s -> %s" % (s1, s2)
    
    

class Variable(Expresion):
    
    def  __init__(self, tok):
        """
        Las variables se inicializan con un identificador
        compuesto por un string con el primer caracter en mayuscula.
        """
        self.id = tok[0]
        
    def reducir(self):
        """
        Las variables reducen a si mismas, tiene que ser sustituidas.
        """
        return self

    def tipar(self, namespace):
        """
        {X : alpha} pertenece a gamma
        ----------------------------
        gamma | > X : alpha
        """
        if not (self.id in namespace):
            for each in namespace:
                print each, namespace[each], each.__class__
            raise TypeException(('No es posible determinar el tipo de la variable %s a' + \
                                'partir del contexto: %s.') % (self.id, namespace))
        return namespace[self.id]
        
    def sustituir(self, var, expresion):
        """
        X {X <- T} --> T
        X {Y <- T} --> X si X != Y
        """
        if self.id == var:
            return expresion
        else:
            return self
     
    @classmethod
    def sintaxis(cls):
        Id = Regex('[A-Z][a-zA-Z]*')
        return Id
    
    def __str__(self):
        return self.id
    
    
class Abstraccion(Expresion):
    
    def __init__(self, toks):
        """
        Una Abstraccion se compone por un id que representa una variable,
        un tipo para esa variable y un expresion.
        """
        var, tipo, expresion = toks
        self.var = var
        self.tipoVar = tipo
        self.expresion = expresion
    
    def reducir(self):
        """
        Una Abstraccion reduce a si misma, es un valor.
        """
        return self
    
    def tipar(self, namespace):
        """
        gamma,{X:alpha} | > M : beta
        ----------------------------
        gamma | > \X:alpha.M : (alpha -> beta)
        """
        nam2 = dict(namespace)
        nam2[self.var] = self.tipoVar
        return Func([self.tipoVar, self.expresion.tipar(nam2)])
        
    def sustituir(self, var, expresion):
        """
        \X:alpha.M {X <- T} --> \X:alpha.M
        \X:alpha.M {Y <- T} --> \X:alpha.(M {Y <- T}) si X != Y
        """
        if self.var != var:
            expresion = self.expresion.sustituir(var, expresion)
            return Abstraccion([self.var, self.tipoVar, expresion])
        return self
        
    @classmethod
    def sintaxis(cls):
        Abs = makeSintaxis('\\',  Id , ':', TipoExp , '.', Exp)
        return Abs
        
    def __str__(self):
        return "\\%s : %s . %s" % (self.var, self.tipoVar, self.expresion)
    
class Aplicacion(Expresion):
    
    def __init__(self, toks):
        """
        Una aplicacion esta compuesta por una funcion aplicadora y
        un parametro.
        """
        aplicador, parametro = toks
        self.aplicador = aplicador
        self.parametro = parametro
    
    def reducir(self):
        """
        Se reduce la funcion aplicadora y el parametro, luego:
        (\X:alpha.M V) --> M {X <- V}
        Finalmente se sustituye M {X <- V} y se reduce M.
        """
        aplicador = self.aplicador.reducir()
        parametro = self.parametro.reducir()
        res = aplicador.expresion.sustituir(aplicador.var, parametro)
        return res.reducir()
        
    def tipar(self, namespace):
        """
        gamma | > M: (alpha -> beta), gamma | > N: alpha
        ------------------------------------------------
        gamma | > (M N) : beta
        """
        x = self.aplicador.tipar(namespace)
        z = self.parametro.tipar(namespace)
        if isinstance(x, Func):
            if x.dominio == z:
                return x.imagen
            else:
                raise TypeException(('Tipo del aplicador: %s \n'+ \
                                    'Tipo del parametro: %s \n'+ \
                                    'El tipo del parametro no se corresponde con el domino del tipo del aplicador.') % (x, z))
        else:
            raise TypeException(('Tipo del aplicador: %s \n'+ \
                                'El tipo del aplicador no se corresponde con el tipo de una Abstraccion.') % x)
    
    def sustituir(self, var, expresion):
        """
       (M N) {X <- T} --> (M {X <- T} N {X <- T})
        """
        aplicador = self.aplicador.sustituir(var, expresion)
        parametro = self.parametro.sustituir(var, expresion)
        return Aplicacion([aplicador, parametro])
    
    @classmethod
    def sintaxis(cls):
        App = makeSintaxis('(', Exp, White().suppress(), Exp,')')
        return App    
    
    def __str__(self):
        return "(%s %s)" % (str(self.aplicador), str(self.parametro))


extensionFunc = Extension('Funciones',
                          expresiones = [Variable, Abstraccion, Aplicacion],
                          tipos = [Func]
                         )
                         
